0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 0 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 8 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 0 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 PiDP
↳9 UsableRulesProof (⇔, 0 ms)
↳10 PiDP
↳11 PiDPToQDPProof (⇒, 30 ms)
↳12 QDP
↳13 MRRProof (⇔, 0 ms)
↳14 QDP
↳15 PisEmptyProof (⇔, 0 ms)
↳16 YES
gopherA_in_ga(nil, nil) → gopherA_out_ga(nil, nil)
gopherA_in_ga(cons(nil, T4), cons(nil, T4)) → gopherA_out_ga(cons(nil, T4), cons(nil, T4))
gopherA_in_ga(cons(cons(nil, T22), T23), cons(nil, cons(T22, T23))) → gopherA_out_ga(cons(cons(nil, T22), T23), cons(nil, cons(T22, T23)))
gopherA_in_ga(cons(cons(cons(T34, T35), T36), T37), T39) → U1_ga(T34, T35, T36, T37, T39, gopherA_in_ga(cons(T34, cons(T35, cons(T36, T37))), T39))
U1_ga(T34, T35, T36, T37, T39, gopherA_out_ga(cons(T34, cons(T35, cons(T36, T37))), T39)) → gopherA_out_ga(cons(cons(cons(T34, T35), T36), T37), T39)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
gopherA_in_ga(nil, nil) → gopherA_out_ga(nil, nil)
gopherA_in_ga(cons(nil, T4), cons(nil, T4)) → gopherA_out_ga(cons(nil, T4), cons(nil, T4))
gopherA_in_ga(cons(cons(nil, T22), T23), cons(nil, cons(T22, T23))) → gopherA_out_ga(cons(cons(nil, T22), T23), cons(nil, cons(T22, T23)))
gopherA_in_ga(cons(cons(cons(T34, T35), T36), T37), T39) → U1_ga(T34, T35, T36, T37, T39, gopherA_in_ga(cons(T34, cons(T35, cons(T36, T37))), T39))
U1_ga(T34, T35, T36, T37, T39, gopherA_out_ga(cons(T34, cons(T35, cons(T36, T37))), T39)) → gopherA_out_ga(cons(cons(cons(T34, T35), T36), T37), T39)
GOPHERA_IN_GA(cons(cons(cons(T34, T35), T36), T37), T39) → U1_GA(T34, T35, T36, T37, T39, gopherA_in_ga(cons(T34, cons(T35, cons(T36, T37))), T39))
GOPHERA_IN_GA(cons(cons(cons(T34, T35), T36), T37), T39) → GOPHERA_IN_GA(cons(T34, cons(T35, cons(T36, T37))), T39)
gopherA_in_ga(nil, nil) → gopherA_out_ga(nil, nil)
gopherA_in_ga(cons(nil, T4), cons(nil, T4)) → gopherA_out_ga(cons(nil, T4), cons(nil, T4))
gopherA_in_ga(cons(cons(nil, T22), T23), cons(nil, cons(T22, T23))) → gopherA_out_ga(cons(cons(nil, T22), T23), cons(nil, cons(T22, T23)))
gopherA_in_ga(cons(cons(cons(T34, T35), T36), T37), T39) → U1_ga(T34, T35, T36, T37, T39, gopherA_in_ga(cons(T34, cons(T35, cons(T36, T37))), T39))
U1_ga(T34, T35, T36, T37, T39, gopherA_out_ga(cons(T34, cons(T35, cons(T36, T37))), T39)) → gopherA_out_ga(cons(cons(cons(T34, T35), T36), T37), T39)
GOPHERA_IN_GA(cons(cons(cons(T34, T35), T36), T37), T39) → U1_GA(T34, T35, T36, T37, T39, gopherA_in_ga(cons(T34, cons(T35, cons(T36, T37))), T39))
GOPHERA_IN_GA(cons(cons(cons(T34, T35), T36), T37), T39) → GOPHERA_IN_GA(cons(T34, cons(T35, cons(T36, T37))), T39)
gopherA_in_ga(nil, nil) → gopherA_out_ga(nil, nil)
gopherA_in_ga(cons(nil, T4), cons(nil, T4)) → gopherA_out_ga(cons(nil, T4), cons(nil, T4))
gopherA_in_ga(cons(cons(nil, T22), T23), cons(nil, cons(T22, T23))) → gopherA_out_ga(cons(cons(nil, T22), T23), cons(nil, cons(T22, T23)))
gopherA_in_ga(cons(cons(cons(T34, T35), T36), T37), T39) → U1_ga(T34, T35, T36, T37, T39, gopherA_in_ga(cons(T34, cons(T35, cons(T36, T37))), T39))
U1_ga(T34, T35, T36, T37, T39, gopherA_out_ga(cons(T34, cons(T35, cons(T36, T37))), T39)) → gopherA_out_ga(cons(cons(cons(T34, T35), T36), T37), T39)
GOPHERA_IN_GA(cons(cons(cons(T34, T35), T36), T37), T39) → GOPHERA_IN_GA(cons(T34, cons(T35, cons(T36, T37))), T39)
gopherA_in_ga(nil, nil) → gopherA_out_ga(nil, nil)
gopherA_in_ga(cons(nil, T4), cons(nil, T4)) → gopherA_out_ga(cons(nil, T4), cons(nil, T4))
gopherA_in_ga(cons(cons(nil, T22), T23), cons(nil, cons(T22, T23))) → gopherA_out_ga(cons(cons(nil, T22), T23), cons(nil, cons(T22, T23)))
gopherA_in_ga(cons(cons(cons(T34, T35), T36), T37), T39) → U1_ga(T34, T35, T36, T37, T39, gopherA_in_ga(cons(T34, cons(T35, cons(T36, T37))), T39))
U1_ga(T34, T35, T36, T37, T39, gopherA_out_ga(cons(T34, cons(T35, cons(T36, T37))), T39)) → gopherA_out_ga(cons(cons(cons(T34, T35), T36), T37), T39)
GOPHERA_IN_GA(cons(cons(cons(T34, T35), T36), T37), T39) → GOPHERA_IN_GA(cons(T34, cons(T35, cons(T36, T37))), T39)
GOPHERA_IN_GA(cons(cons(cons(T34, T35), T36), T37)) → GOPHERA_IN_GA(cons(T34, cons(T35, cons(T36, T37))))
GOPHERA_IN_GA(cons(cons(cons(T34, T35), T36), T37)) → GOPHERA_IN_GA(cons(T34, cons(T35, cons(T36, T37))))
cons2 > GOPHERAINGA1
GOPHERA_IN_GA_1=1
cons_2=0